$M$.pre($a$,$s$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; (($M$.2.2.2).1); $a$; $a$,$P$.($\uparrow$($P$($s$))))